A, B:Type, f:(A(B + Top)), ds:(IdType), da:(IdKndType), X:Interface(ds;da;A), es:ES.
es-decl(es;ds;da)  ([[interface-compose(f;X)]] = f o [[X]]    AbsInterface(B)) 

latex

Definitions

s ~ t, interface-compose(f;X), in-interface(es;X;e), Knd, Id, f(a), AbsInterface(A), [[X]], f o g  , can-apply(f;x), do-apply(f;x), fpf dom compose compseq tag def, Unit, P  Q, P & Q, x:A. B(x), P  Q, , <a, b>, if b then t else f fi , interface-val(es;X;e), left + right, Top, ff, s = t, t  T, A, False, E, t.1, es-decl(es;ds;da), ES, b, x:A  B(x), Interface(ds;da;A), a:A fp B(a), x:AB(x), Type, fpf ap compose compseq tag def, f(x)

Lemmas

interface-val wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, abs-interface wf, p-compose wf